\begin{tabbing}
rel\_exp($T$; $R$; $n$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if ($n$ =$_{0}$ 0)\+
\\[0ex]then $\lambda$$x$,$y$. $x$ = $y$
\\[0ex]else $\lambda$$x$,$y$. $\exists$$z$:$T$. (($x$ $R$ $z$) $\wedge$ ($z$ rel\_exp($T$; $R$; ($n$ {-} 1)) $y$))
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]rel\_exp($T$; $R$; $n$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if ($n$ =$_{0}$ 0)\+
\\[0ex]then $\lambda$$x$,$y$. $x$ = $y$ $\in$ $T$
\\[0ex]else $\lambda$$x$,$y$. $\exists$$z$:$T$. (($x$ $R$ $z$) $\wedge$ ($z$ rel\_exp($T$; $R$; ($n$ {-} 1)) $y$))
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}